Nuprl Lemma : bool_ind
9,38
postcript
pdf
P
:(
).
P
(ff)
P
(tt)
{
b
:
.
P
(
b
)}
latex
ProofTree
Definitions
t
T
,
{
T
}
,
x
(
s
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
Unit
,
,
,
tt
,
ff
Lemmas
bfalse
wf
,
btrue
wf
,
bool
wf
origin
P:(
). P(ff) 
P(tt) {b:. P(b)}
P:(). P(ff) P(tt) {b:. P(b)}
T Qx:A. B(x)